Problem:
0(1(0(x1))) -> 0(2(3(1(3(0(x1))))))
0(2(1(x1))) -> 3(1(3(0(2(x1)))))
0(2(1(x1))) -> 0(2(3(3(1(3(x1))))))
0(2(1(x1))) -> 0(4(3(1(3(2(2(x1)))))))
0(2(1(x1))) -> 0(2(3(2(2(1(3(2(x1))))))))
1(0(0(x1))) -> 2(3(1(3(0(0(x1))))))
0(0(2(0(x1)))) -> 0(0(4(4(3(2(0(x1)))))))
0(1(2(1(x1)))) -> 0(3(1(3(1(3(2(x1)))))))
0(1(3(5(x1)))) -> 0(5(4(4(3(1(4(x1)))))))
0(1(3(5(x1)))) -> 3(5(4(3(1(3(2(0(x1))))))))
0(1(5(1(x1)))) -> 5(3(1(3(0(1(x1))))))
0(2(1(4(x1)))) -> 0(3(2(2(1(4(x1))))))
0(2(1(4(x1)))) -> 3(2(1(0(4(3(x1))))))
0(2(2(1(x1)))) -> 3(2(0(2(3(1(x1))))))
0(2(2(5(x1)))) -> 3(1(3(2(2(0(4(5(x1))))))))
0(2(4(4(x1)))) -> 3(2(0(4(4(5(4(x1)))))))
0(2(4(5(x1)))) -> 3(2(0(4(5(x1)))))
0(3(3(4(x1)))) -> 5(4(3(2(3(0(x1))))))
0(3(5(1(x1)))) -> 5(4(3(2(2(0(1(x1)))))))
1(0(2(4(x1)))) -> 2(3(0(3(1(4(x1))))))
1(1(2(5(x1)))) -> 1(3(2(2(1(5(x1))))))
0(0(0(3(4(x1))))) -> 0(0(4(4(5(2(3(0(x1))))))))
0(0(1(1(5(x1))))) -> 5(0(3(1(3(1(0(5(x1))))))))
0(1(2(2(4(x1))))) -> 4(3(2(1(2(3(0(x1)))))))
0(1(5(1(4(x1))))) -> 5(3(1(0(4(3(1(x1)))))))
0(2(2(0(1(x1))))) -> 0(4(3(0(2(3(2(1(x1))))))))
0(2(2(2(5(x1))))) -> 3(2(2(5(4(3(2(0(x1))))))))
0(2(2(5(0(x1))))) -> 3(2(2(0(5(2(3(0(x1))))))))
0(3(4(1(4(x1))))) -> 2(3(3(1(0(5(4(4(x1))))))))
0(4(1(3(4(x1))))) -> 3(1(3(0(4(4(5(x1)))))))
0(4(2(2(4(x1))))) -> 3(2(2(0(4(4(x1))))))
0(4(2(4(1(x1))))) -> 3(1(0(4(4(3(2(x1)))))))
0(5(2(1(5(x1))))) -> 5(4(5(2(3(1(0(x1)))))))
1(0(2(2(4(x1))))) -> 2(2(0(4(3(1(4(x1)))))))
1(0(2(2(4(x1))))) -> 2(3(3(2(1(0(4(3(x1))))))))
1(2(2(0(1(x1))))) -> 4(3(2(1(0(2(3(1(x1))))))))
1(2(3(5(0(x1))))) -> 5(2(3(1(3(0(x1))))))
1(2(4(3(5(x1))))) -> 5(4(3(1(3(2(x1))))))
0(0(1(3(3(5(x1)))))) -> 0(3(2(3(0(1(5(x1)))))))
0(0(2(2(3(0(x1)))))) -> 0(2(3(0(3(2(0(x1)))))))
0(0(2(2(5(1(x1)))))) -> 0(3(0(2(3(2(1(5(x1))))))))
0(0(3(5(3(0(x1)))))) -> 0(5(0(3(1(3(3(0(x1))))))))
0(0(4(0(5(1(x1)))))) -> 0(0(4(0(4(3(1(5(x1))))))))
0(0(4(1(3(0(x1)))))) -> 0(0(3(2(3(0(1(4(x1))))))))
0(1(0(3(4(5(x1)))))) -> 3(1(0(4(3(5(0(4(x1))))))))
0(1(4(0(2(5(x1)))))) -> 0(5(2(0(4(4(1(x1)))))))
0(1(5(3(4(0(x1)))))) -> 0(4(4(2(0(3(1(5(x1))))))))
0(2(1(5(3(5(x1)))))) -> 3(2(1(3(5(1(5(0(x1))))))))
0(3(5(2(4(1(x1)))))) -> 0(0(5(4(3(2(1(x1)))))))
0(5(0(1(5(4(x1)))))) -> 3(1(3(0(0(5(4(5(x1))))))))
0(5(1(1(3(4(x1)))))) -> 4(1(0(4(5(4(3(1(x1))))))))
0(5(3(4(1(4(x1)))))) -> 5(4(0(4(3(1(3(x1)))))))
0(5(3(4(1(5(x1)))))) -> 0(3(2(1(0(5(4(5(x1))))))))
0(5(5(0(1(5(x1)))))) -> 0(5(5(3(2(1(5(0(x1))))))))
1(0(2(4(0(5(x1)))))) -> 1(4(0(3(2(3(0(5(x1))))))))
1(1(4(0(1(0(x1)))))) -> 0(3(1(3(1(4(1(0(x1))))))))
1(2(1(0(2(1(x1)))))) -> 1(1(3(2(0(2(1(x1)))))))
1(2(4(0(3(4(x1)))))) -> 3(2(0(4(3(3(1(4(x1))))))))
1(2(4(3(3(0(x1)))))) -> 4(0(2(3(3(1(3(0(x1))))))))
1(2(4(3(3(5(x1)))))) -> 3(2(3(2(5(4(3(1(x1))))))))
1(2(4(3(4(5(x1)))))) -> 3(1(3(2(4(5(4(x1)))))))
1(2(4(5(1(0(x1)))))) -> 0(4(2(1(3(1(5(x1)))))))
1(2(4(5(3(4(x1)))))) -> 4(3(2(2(1(3(5(4(x1))))))))
1(2(5(5(3(0(x1)))))) -> 5(2(3(3(1(3(5(0(x1))))))))
0(0(2(4(5(3(5(x1))))))) -> 2(0(5(4(3(5(3(0(x1))))))))
0(1(0(5(3(5(1(x1))))))) -> 1(0(0(5(5(3(1(3(x1))))))))
0(1(2(2(5(2(0(x1))))))) -> 5(1(0(3(2(2(2(0(x1))))))))
0(2(1(5(4(0(1(x1))))))) -> 0(0(5(1(2(3(1(4(x1))))))))
0(2(3(4(1(1(4(x1))))))) -> 3(1(0(4(4(1(2(0(x1))))))))
0(2(4(1(1(5(1(x1))))))) -> 3(1(0(5(4(1(1(2(x1))))))))
0(2(5(0(4(0(1(x1))))))) -> 0(5(1(0(4(3(2(0(x1))))))))
0(2(5(5(3(5(1(x1))))))) -> 0(5(5(1(5(5(3(2(x1))))))))
0(4(0(3(5(2(0(x1))))))) -> 0(4(0(4(5(3(2(0(x1))))))))
0(4(1(1(4(1(5(x1))))))) -> 0(4(3(1(4(1(1(5(x1))))))))
0(4(1(4(0(3(5(x1))))))) -> 3(1(5(0(0(4(3(4(x1))))))))
0(5(1(3(4(2(4(x1))))))) -> 5(4(4(0(3(1(5(2(x1))))))))
1(0(3(3(3(4(0(x1))))))) -> 0(3(0(3(3(1(4(5(x1))))))))
1(0(3(4(4(3(5(x1))))))) -> 5(4(3(1(3(0(2(4(x1))))))))
1(2(0(4(1(3(5(x1))))))) -> 5(4(2(3(1(4(1(0(x1))))))))
1(2(4(0(5(3(5(x1))))))) -> 5(1(3(2(3(5(0(4(x1))))))))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5}
transitions:
41(187) -> 188*
41(57) -> 58*
41(47) -> 48*
41(17) -> 18*
41(139) -> 140*
41(59) -> 60*
41(44) -> 45*
41(71) -> 72*
41(51) -> 52*
41(46) -> 47*
41(108) -> 109*
41(115) -> 116*
41(95) -> 96*
31(70) -> 71*
31(65) -> 66*
31(182) -> 183*
31(142) -> 143*
31(112) -> 113*
31(144) -> 145*
31(114) -> 115*
31(94) -> 95*
31(186) -> 187*
31(21) -> 22*
31(168) -> 169*
31(138) -> 139*
31(68) -> 69*
31(23) -> 24*
21(20) -> 21*
21(167) -> 168*
21(127) -> 128*
21(97) -> 98*
21(184) -> 185*
21(129) -> 130*
21(69) -> 70*
21(49) -> 50*
21(19) -> 20*
21(141) -> 142*
21(111) -> 112*
21(143) -> 144*
21(93) -> 94*
21(185) -> 186*
21(135) -> 136*
11(157) -> 158*
11(137) -> 138*
11(22) -> 23*
11(169) -> 170*
11(159) -> 160*
11(183) -> 184*
11(113) -> 114*
11(165) -> 166*
51(45) -> 46*
51(25) -> 26*
51(72) -> 73*
51(116) -> 117*
51(96) -> 97*
51(31) -> 32*
51(16) -> 17*
51(33) -> 34*
51(140) -> 141*
01(85) -> 86*
01(67) -> 68*
01(109) -> 110*
01(91) -> 92*
01(83) -> 84*
01(48) -> 49*
01(18) -> 19*
00(2) -> 5*
00(4) -> 5*
00(1) -> 5*
00(3) -> 5*
10(2) -> 6*
10(4) -> 6*
10(1) -> 6*
10(3) -> 6*
20(2) -> 1*
20(4) -> 1*
20(1) -> 1*
20(3) -> 1*
30(2) -> 2*
30(4) -> 2*
30(1) -> 2*
30(3) -> 2*
40(2) -> 3*
40(4) -> 3*
40(1) -> 3*
40(3) -> 3*
50(2) -> 4*
50(4) -> 4*
50(1) -> 4*
50(3) -> 4*
1 -> 159,129,85,57,31
2 -> 137,111,67,44,16
3 -> 165,135,91,59,33
4 -> 157,127,83,51,25
20 -> 65*
24 -> 86,68,93,5
26 -> 17*
32 -> 17*
34 -> 17*
45 -> 108*
46 -> 182*
47 -> 167*
50 -> 23*
52 -> 45*
58 -> 45*
60 -> 45*
66 -> 92,86,68,93,5
68 -> 93*
73 -> 68,93,5
84 -> 68*
86 -> 68*
92 -> 68*
98 -> 19*
110 -> 97*
117 -> 160,138,6
128 -> 112*
130 -> 112*
136 -> 112*
145 -> 160,138,6
158 -> 138*
160 -> 138*
166 -> 138*
170 -> 144*
188 -> 160,138,6
problem:
Qed